Add Quint model of Interchain Security #1336
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This reverts commit 1320b95.
insumity
reviewed
Oct 12, 2023
Co-authored-by: insumity <[email protected]>
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
| ) | ||
| ) | ||
| ).with( | ||
| // put an entry into sentVscPacket on the provider that corresponds to the packet we put on the consumer |
There was a problem hiding this comment.
Suggested change
| // put an entry into sentVscPacket on the provider that corresponds to the packet we put on the consumer | |
| // put an entry into sentVscPacketsToConsumer on the provider that corresponds to the packet we put on the consumer |
I guess the packet put on the consumer is the maturation packet?
There was a problem hiding this comment.
the VSC packet is sent to the consumer, the consumer responds with a VSCMatured packet
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
insumity
reviewed
Oct 12, 2023
insumity
approved these changes
Oct 12, 2023
konnov
reviewed
Oct 12, 2023
bermuell
reviewed
Oct 13, 2023
| val newConsumerStatus = res1._1 | ||
| val err1 = res1._2 | ||
| val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) | ||
| val err2 = res2._2 |
There was a problem hiding this comment.
no need to run stopConsumers in case of error on startConsumers, right?
There was a problem hiding this comment.
Technically not, no, but it doesn't hurt and I think it's slightly more readable like this. (Performance is not really an issue for models, we should likely radically prefer readability unless we have evidence certain things need to be faster). If you think it's currently less readable than the alternative, lmk and I will adjust
There was a problem hiding this comment.
Not just performance but alos readability. With constructs like this it means to me that other steps have to be executed until you return, but maybe it's just me. Up to you as it's not an issue.
konnov
reviewed
Oct 16, 2023
p-offtermatt
force-pushed
the
ph/quint-model-v2
branch
from
38010c8 to
b817f43
Compare
bermuell
approved these changes
Oct 17, 2023
MSalopek
pushed a commit
that referenced
this pull request
Dec 1, 2023
* Start new attempt on Quint model of ICS * Advance quint model * Add first finished draft of model * Add test run to model * Rename model, add test, use powerset for nondeterminism * Reintroduce vsc changed tracking variables * Add text with what expliticly is modelled * Add bluespec to ccv.qnt * Add bluespec to expraSpells.qnt * Add docstring to extraSpells module * Start rewriting model * Revert "Start rewriting model" This reverts commit 1320b95. * Start rewriting quint model * Continue seperating logic in Quint model * Start debugging cryptic error message * Start adding endAndBeginBlock defs * Diagnose Quint parser bug * Fix type in Quint * Add endBlock actions * Start adding state machine module * Save status with crashing effect checker * Resolve issue by removing undefined field * Remove add * Fix init * Snapshot spec with parser crasher * Snapshot model * Start debugging tests * Finish test for quint model * Add README and improve folder structure * Fix import * Add some invariants * Refactor Consumer advancement * Snapshot error * Make time module upper case * Add invariants * Clean up invariants * Add script to run many invariants * Update model * Update model for bug reporting] * Remove sanity check script * Fix model and randomly run invariant checks * Remove trace * Add model checking to README * Add bluespec * Try fixed bluespec * Fix bluespec definitions * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Fix minor issues * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Correct verify command by adding \ * Add Inv to ValidatorUpdatesArePropagated * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Apply comments * Rename VSC to Vsc * Return plain ProtocolState in cases where no error is returned anyways * Remove unused defs * Fix indentation * Rename to isRunningConsumer * Unify naming for extraSpells * Remove HasSubsequence * Run tests before running invariants * Rename modules to have same name as files * Adjust module name in README and invariant script * Fix voting power change behaviour around 0 * Adjust error message in test * Remove special treatment of 0 voting power * Rename sentVscPackets to sentVscPacketsToConsumer * Update tests/difference/core/quint_model/README.md Co-authored-by: insumity <[email protected]> * Resolve comments * Adjust comment to fit actual time advancement * Remove hasError field and make it a function * Adjust docstring * Remove unused timedout val * Update doc * Rename statemachine to model * Use ... syntax * Change Error type to string --------- Co-authored-by: insumity <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Closes: #1239
This adds a quint model of interchain Security, based on the existing TLA+ model by @Kukovec.
There are a few notable differences:
Other than that, some implementation details are different. Some are my preference, some are just due to what is more natural to write in Quint, some are to (hopefully) make traces that are easier to use.
How to review: